Valtype($k$;${\it da}$;${\it din}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$kindcase($k$; $a$.${\it da}$($a$)?Top; $l$,${\it tg}$.${\it din}$($\langle$$l$$,\,$${\it tg}$$\rangle$)?Top )